Issue3823.agda:16,13-14
No module M in scope
when scope checking record { M }
